
\title{}
\author{}
\date{\today}

\documentclass[11pt]{article}

\usepackage[paper=a4paper,dvips,top=1.5cm,left=1.5cm,right=1.5cm,
    foot=1cm,bottom=1.5cm]{geometry}

\usepackage{amsmath}
\usepackage{mathtools}

%\usepackage{dsfont} % for \mathds{N}


\begin{document}
 \maketitle


% \begin{abstract}
% \end{abstract}

\section{Questions}

\subsection{Initial Questions}
\begin{enumerate}
  \item Is it possible to get a deadlock as a result of adding atomic sections (where one didn't exist before)?
  \item Is it possible to get a livelock as a result of adding atomic sections (where one didn't exist before)?
  \item Is it possible to violate wait freedom as a result of adding atomic sections (where one did hold before)?
  \item Is it possible to violate lock freedom as a result of adding atomic sections (where one did hold before)?
  \item Is it possible to violate obstruction freedom as a result of adding atomic sections (where one did hold before)?
  \item What effect has the scheduler fairness/non fairness on the previous questions/answers?
  \item What kind of fairness assumptions we have on the environment? are there any besides the scheduler fairness?
  \item What kind of methods are there for verifying termination/liveness-properties for concurrent programs?
  \item For each method of verifying liveness-properties:
        \begin{enumerate}
        \item What liveness-property can it verify?
        \item What kind of pre-assumptions does it need?
        \item Is fairness an encoded part of the method, or should it be assumed?
        \item Efficiency?
        \end{enumerate}
\end{enumerate}


\subsection{Remarks for Initial  Questions}
\begin{verbatim}
wait freedom --> lock freedom --> obstruction freedom

wait freedom --> no deadlock and no starvation(no livelock)
lock freedom --> no deadlock
\end{verbatim}


\begin{enumerate}
  \item Deadlock: a Deadlock occurs when two or more processes (programs in execution) request the same resources and are allocated them in such a way that a circular chain of processes is formed, where each process is waiting for a resource held by the next process in the chain\footnote{http://www.britannica.com/EBchecked/topic/130675/computer-science/21955/Deadlock-and-synchronization?anchor=ref384124}
      According to a definition of atomic section I saw \footnote{Lomet, D. B. Process structuring, synchronization, and recovery using atomic actions, Proc. ACM 80
Conf. on Language Design for Reliable Software, SIGPLAN Notices 12, 3 (Mar. 1977) pp. 128-137
} :
\begin{enumerate}\item An action is atomic if the process performing it is not aware of the existence of any other active process (can detect no spontaneous change) and no other process is aware of the activity of this process (its state changes are concealed) during the time the process is performing the action.
\item An action is atomic if the process performing it does not communicate with other processes while it is executing the action.
\item Actions are atomic if they can be considered, so far as other processes are concerned, to be indivisible and instantaneous, such that the effect on the system are as if they were interleaved as opposed to concurrent.\end{enumerate}Since according to that definition a thread in an atomic section cannot communicate with other threads it is not reasonable that it will wait for a resource. Thus an adding of an atomic section cannot add a deadlock.

  \item Livelock:
    Under fairness assumption: 'If a context switch can occur then at some point in the future it will'.
    The original program:
    \begin{verbatim}
           initial x = 0, y =0;
           thread0: { while (x % 2 == 0) y=1;  }
           |
           thread1: { while (y!=1) { x++;} }            
    \end{verbatim}
    And the modified program:
    \begin{verbatim}
           initial x = 0, y =0;
           thread0: {  atomic{while (x % 2 == 0) y=1;} }
            ||
           thread1: { while (y!=1) { x++; } }  
    \end{verbatim}        
      Under fairness assumption: 'If a transition is enabled, it will be taken some time in the future'.
       The original program:
       \begin{verbatim}
       initial x = 0, y =0;
       thread0: { while (x % 2 ==0) y=1;  }
       ||
       thread1: { while (y!=1) { x++; x++ } } 
       \end{verbatim} 
         And the modified program:
       \begin{verbatim} 
       initial x = 0, y =0;
       thread0: { while (x % 2 ==0) y=1;  }
        ||
       thread1: { while (y!=1) { atomic {x++; x++ } } }  
       \end{verbatim}
  \item Wait freedom: If the previous example is valid then by it and the postulation wait freedom implies no livelock,
        the answer is positive.
  \item
  \item
  \item
  \item
  \item
  \item
        \begin{enumerate}
        \item
        \item
        \item
        \item
        \end{enumerate}
\end{enumerate}

\subsection{How do we add thread modular reasoning to AGS?}
\emph{Initial blueprint}
     \begin{enumerate}
      \item build transition systems for $T_1$, $T_2$ assuming some environment for each.
        \item while there exists 
		\( 
 			\pi_1 \in \left[\kern-0.15em\left[  T_1  \right]\kern-0.15em\right] s.t. \pi_1 \not\models spec
		\) 
		or
		\( 
 			\pi_2 \in \left[\kern-0.15em\left[  T_2  \right]\kern-0.15em\right] s.t. \pi_2 \not\models spec
		\) 

		\begin{enumerate}
		\item choose $\pi$ and either
			\begin{enumerate}
			\item avoid ( $\pi$ ) 
			\item or refine ( environment / $\alpha$ )
			\end{enumerate}
		\end{enumerate}
        \end{enumerate}

\emph{Missing / In need of definition} \\
What is the input of the algorithm? \\
How are the environment assumptions built into $T_1$ and $T_2$ transition system. What assumptions are those? \\
What does it mean for a path(in modular context) to satisfy a specification(in global context)? \\
How does one "abstract" a specification? \\
How does one know if there are more "bad" paths? \\
How does one find/choose the next "bad" paths? \\
What information does a path hold? \\
How do you avoid a bad path? (relates to what information does it hold) \\
How do you refine the environment? \\
How do you refine the abstraction? Do you refine it for all the transition systems?\\
Abstract to several threads? \\


\subsection{Definitions (2 threads) }
\paragraph{Basic constructs} We shall assume there are 2 threads. Let's denote a vector \(g \in G\) as representing an evaluation of global variables, and vectors \( l_1 \in \L_1 \), \( l_2 \in \L_2 \) as representing an evaluation of local variables for threads 1,2 (including the corresponding program counter).
\paragraph{Transition system} - Here we shall have a global  transition system \( \langle\Sigma, T, Init\rangle \) 
where:\\
 \(\Sigma=(G\times T_1 \times T_2) \) is a set of states (containing possible instantiations of global and local variables to each thread, program counters etc.). 
\(T \subseteq \Sigma\times\Sigma  \) is a sets of transitions between states and \( Init \subseteq \Sigma\) are the initial states.\\
\paragraph{path}For a transition system ts, a path, $\pi$ is a (possibly infinite) sequence of states \(\pi_0,\pi_1,...\) such that for each $k$ the transition \( (\pi_k,\pi_{k+1}) \in T\).
%do we want it to start from the initial state?

\paragraph{Abstraction} - Initially we shall consider thread modularity as the single abstraction presented.
We shall add a transition system for each thread \( i\in\{1,2\} \langle\Sigma_i, T_i, Init_i\rangle \), where \( \Sigma_i \) contains the projection of the states to the domain of thread $i$, meaning \( \Sigma_1=\{(g,l_1)\mid \exists l_2 \in L_2 s.t. (g,l_1,l_2) \in \Sigma\}\), \\  \(T_i \subseteq \Sigma_i\times\Sigma_i  \) are sets of transitions between states and  \(Init_i\subseteq\Sigma_i\)are the initial states, which will also hold the environment assumptions.\\
$T_1$ will hold the projection of the transitions in $T$ to the domain of thread 1.
\[ \{((g,l_1),(g',l'_1)) \mid \exists l_2,l'_2 \in L_2 s.t. ((g,l_1,l_2),(g',l'_1,l_2))\in T\}\subseteq T_1\]
Initially no assumption is made regarding the environment - meaning at each step the environment can change any of the global variables.
 \\--\\do we add 3-value logic?\\ how do we say that we have an assumption on the environment? \\ do we add special nodes as in Barabara games notation?\\ 
do we use Flanagen-Quadeer? add rules, and find lfp? \\ Cartesian Abstract Interpretation? They work with sets, I want to work with states- right?\\--\\
Essentially to my opinion the question is what to do at the refine stage along with what representation of the modularity in the  transition system.

\paragraph{Rybalchenko Indeterminism solution} - Intuitively we add nodes that represent the environment and the restrictions on it.
We define instead of \( \Sigma_1,\Sigma_2 \) new groups  \(\Gamma_1,\Gamma_2\) where \(\Sigma_i \subseteq \Gamma_i\) and we add states of the form \(([\phi(g)],l_1)\) where $\phi$ is a formula restricting g.
(making \(\Gamma_1\subseteq(\Sigma_1\cup (Equation(G)\times L_1) )\) where Equation is the domain of all possible restriction, for simplicity lets say that for each \( g \in G \) Equation($g$)=\(\{g-c1\le g \le g+c2 \mid 0\le c1,c2 \}\) (written as if it is a single global variable and extention of the idea to vectors)\\
In abuse of notation the transitions will now be \(T_i \subseteq \Gamma_i\times\Gamma_i  \)  containing the previous transitions and for each transition \( ((g,l_1),(g',l'_1)) \) we shall add two transitions  
\( ((g,l_1),(\phi(g),l'_1)) \) \\--\\I want to propagate the change in the variables, but I can't? it's as if I have numeric values. I have the values of the variables not the effect of the instructions on them.
The idea being that once we reach a failed execution we can refine the environment by effecting the restrictions on the change in $\phi(g)$ I think this means that my intention is a constant $\phi$ throughout the 
first thread representing the possible effect the second thread can have on the global variables.\\
The restriction is done by passing through the transition system of the second thread and approximating the possible changes that mught be made to the global variable. possibly unbounded. As the iteration progress mutual information becomes more available and finer restriction on the effect of thread 2 will be denoted in $phi$.
 
\paragraph{Rybalchenko Cartesian Abstract Interpertation}

\( D=2^{\Sigma} \) the set underlying  the concrete lattice.\\
\(D^\#=2^{\Sigma_1}\times2^{\Sigma_1}\) is the set underlying the abstract lattice,\\
\(\alpha_{cart}:D \to D^\#, S \mapsto (S_1,S_2) where S_1={ (g,l_1) \mid (g,l_1,\_)\in S}\\  S_2={ (g,l_2) \mid (g,\_,l_2)\in S}\) \\
\(\gamma_{cart}:D^\# \to D, (S_1,S_2) \mapsto S where S={ (g,l_1,l_2) \mid (g,l_1)\in S_1 and (g,l_2)\in S_2}\)\\
We don't have traces in this paper, but it fits better to AGS framework.
The declarations give us \((\Sigma_1, \Sigma_2) = \alpha(\Sigma) \). \\
The refinement is depicted in the transition systems.\\
Starting with(may arcs) \[T_1 = \{ ((g,l_1),(g',l'_1)) \mid \exists l_2,l'_2 s.t (g,l_1,l_2)\in \gamma((g,l_1)) and (g',l'_1,l'_2)\in \gamma((g',l'_1)) and ((g,l_1,l_2),(g',l'_1,l'_2))\in T\} \]
Then the refinement is CEGAR.

%\bibliographystyle{abbrv}
%\bibliography{main}

\end{document}
This is never printed 


